System F
#Fleeting_Notes
System F
Girardの多相ラムダ計算(polymorphic lambda calculus)
Girard-Reynolds多相ラムダ計算とも言いそう
単純型付きラムダ計算 + 多相型(ポリモーフィズム)
全称型
ラムダ・キューブの$ \lambda 2 はSystem Fと等価
($ \uparrow λ→) → λ2
単純型付きラムダ計算 + 多相型
二階型付きラムダ計算
工学部専門科目「計算と論理」配布資料 多相ラムダ計算 (System F)
二階述語論理と対応がある
確認用
Q. System F
関連
System U
System Fω
『Type Theory and Applications』
メモ
Wadler, P. (1989). Theorems for free!.
System Fを用いて、型からプログラムの性質を導出する手法を提案した論文。型理論の実用的な側面や型安全性の応用を学ぶのに役立つ。
PDF: https://people.mpi-sws.org/~dreyer/tor/papers/wadler.pdf
調査用
Google.icon System F(日)
Google.icon System F(英)
Wikipedia.icon
System F - Wikipedia(日)
System F(検索) - Wikipedia(日)
Wikipedia.icon
System F - Wikipedia(英)
System F(検索) - Wikipedia(英)